\begin{tabbing}
$\forall$${\it es}$:ES.
\\[0ex]($\forall$$e$:E. state after $e$ $=$ Trans(loc($e$))(kind($e$),val($e$),(state when $e$)) $\in$ state@loc($e$))
\\[0ex]\& (\=$\forall$$e$:E.\+
\\[0ex]islocal(kind($e$))
\\[0ex]$\Rightarrow$ \=isl(Choose(loc($e$))(act(kind($e$)),(state when $e$)))\+
\\[0ex]\& val($e$) $=$ outl(Choose(loc($e$))(act(kind($e$)),(state when $e$))) $\in$ valtype($e$))
\-\-\\[0ex]\& (\=$\forall$$e$:E.\+
\\[0ex]isrcv(kind($e$))
\\[0ex]$\Rightarrow$ ($\langle$lnk(kind($e$))$,\,$tag(kind($e$))$,\,$val($e$)$\rangle$ $\in$ \=Send(loc(sender($e$)))\+
\\[0ex](kind(sender($e$))
\\[0ex],val(sender($e$))
\\[0ex],(state when sender($e$)))))
\-\-
\end{tabbing}